es:ES, T:Type, i:Id, P:(T
Prop), L:T List, Q:(E{x:T| (x 
L) }Prop).
(
x:T. Dec(P(x)))
(xL. e:E. Q(e,x) loc(e) = i Id)
(xL. P(x) (
e:E. Q(e,x)))
(
(xL.P(x)) e'@i.True)
e'@i.xL. P(x) (e:E. e 
e' & Q(e,x)) | 0,22 |
es:ES, T:Type, i:Id, P:(TProp), L:T List, Q:(E{x:T| (x L) }Prop).
x:T. Dec(P(x)))
(xL. e:E. Q(e,x) loc(e) = i Id)
(xL. P(x) (e:E. Q(e,x)))
((xL.P(x)) e'@i.True)
e'@i.xL. P(x) (e:E. e e' & Q(e,x))
| Definitions | x:A. B(x)  x. t(x)xL.P(x))A Qe@i.P(e)x:A. B(x)xL. P(x) T T l) T B e' |
| Lemmas |